es  es' mod es,e.P(es;e)
== {e:E| P(es;e)}   {e:E| P(es';e)} 
== & (e:{e:E| P(es;e)} . kind(e) = kind(e) & loc(e) = loc(e))
== & (e1, e2:{e:E| P(es;e)} .
== & (((e1 < e2)  (e1 < e2)) & (val(e1)  val(e2)  val(e1)  val(e2))) 

latex

---

clarification:

es  es' mod es,e.P(es;e)
== {e:es-E(es)| P(es;e)}   {e:es-E(es')| P(es';e)} 
== & (e:{e:es-E(es)| P(es;e)} .
== & (es-kind(es; e) = es-kind(es'; e)  Knd & es-loc(es; e) = es-loc(es'; e)  Id)
== & (e1:{e:es-E(es)| P(es;e)} , e2:{e:es-E(es)| P(es;e)} .
== & ((es-causl(es; e1; e2)  es-causl(es'; e1; e2))
== & (& (es-same-val(es;e1;e2)  es-same-val(es';e1;e2))) 

latex

Definitions	A  B, Knd, kind(e), s = t, Id, loc(e), x:A. B(x), {x:A| B(x)} , E, P & Q, (e < e'), P  Q, val(e)  val(e')
FDL editor aliases	es-p-equiv